es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p,
q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
[e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  e1  e2  

latex

Definitions	P & Q, x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), ES, t  T, x:A. B(x), E, loc(e), Id, Prop, x(s1,s2), x,y. t(x;y), e  e' , P  Q, , , ij, False, A, AB, {T}, SQType(T), 1of(t), i  j < k, {i..j}, Trans x,y:T. E(x;y), (e <loc e'), P  Q
Lemmas	es-le-trans, le wf, es-le wf, es-le-self, ge wf, nat properties, nat wf, es-pstar-q wf, Id wf, es-loc wf, es-E wf, event system wf